Tute (Week 8)

Use MinHS type constructors \(+\), \(\times\) and \(\mathbf{rec}\) to describe types isomorphic to each of the following Haskell types. Give example terms for each type.

data Direction = East | West | North | South
data Foo = Foo Int Bool Int
data Tree = Node Tree Tree | Leaf

Give an example MinHS term for each of the following types (if such a term exists), and derive the typing judgement for that term.

1. \(\mathbf{rec}\ t.\ (\mathtt{Int} + t)\)
2. \(\mathbf{rec}\ t.\ (\mathtt{Int} \times \mathtt{Bool})\)
3. \(\mathbf{rec}\ t.\ (\mathtt{Int} \times t)\)

Which of the following types are isomorphic to each other (assuming a strict semantics)?

1. \(\textbf{rec}\ t.\ t \times t\)
2. \(\textbf{0}\)
3. \(\textbf{1}\)
4. \(\textbf{1} \times \textbf{0}\)
5. \(\textbf{rec}\ t.\ t \times \textbf{1}\)
6. \(\textbf{rec}\ t.\ t + \textbf{1}\)

For each of the following terms, give a possible type for the term (there may be more than one type).

1. \((\mathsf{InL}\ \mathsf{True})\)
2. \((\mathsf{InR}\ \mathsf{True})\)
3. \((\mathsf{InL}\ (\mathsf{InL}\ \mathsf{True}))\)
4. \((\mathsf{roll}\ (\mathsf{InR}\ \mathsf{True}))\)
5. \((\texttt{()}, (\mathsf{InL}\ \texttt{()}))\)

Explain the difference between a function of type \(\forall a.\ a \rightarrow a\) and \((\forall a.\ a) \rightarrow (\forall a.\ a)\).

What can we conclude about the following functions solely from looking at their type signature?

1. \(f_1 : \forall a.\ [a] \rightarrow a\)
2. \(f_2 : \forall a.\ \forall b.\ [a] \rightarrow [b]\)
3. \(f_3 : \forall a.\ \forall b.\ [a] \rightarrow b\)
4. \(f_4 : [\texttt{Int}] \rightarrow [\texttt{Int}]\)